『An Extensible User Interface for Lean 4』

Nawrocki, Wojciech, Ayers, Edward W., Ebner, Gabriel. An Extensible User Interface for Lean 4. 2023, p. 20 pages, 1531949 bytes.

1. どんなもの？

Lean 4のProofWidgets4による、より良い証明のビジュアライゼーション

2. 先行研究と比べてどこがすごい？

3. 技術や手法のキモはどこ？

4. どうやって有効だと検証した？

5. 議論はある？

6. 次に読むべき論文は？

============================

table:用語

Interactive theorem proving(ITP) インタラクティブな定理証明？